k:Knd, T, A, B:Type, l:IdLnk, x, tg:Id, f:(ABT), c:(AB), es:ES.
k(v:B) sends
kf(x:A,v) on
kl tagged with tg:T
kprovided c(x,v)
 (g:{e:E| loc(e) = source(l)  Id & kind(e) = k & ((c((x when e),val(e))))} E
 ((e:{e:E| loc(e) = source(l)  Id & kind(e) = k & ((c((x when e),val(e))))} .
 ((kind(g(e)) = rcv(l,tg)  Knd)
 (c (sender(g(e)) = e
 (c & (e'':E. (kind(e'') = rcv(l,tg)  Knd)  (sender(e'') = e)  (e'' = g(e)))
 (c & val(g(e)) = f((x when e),val(e))))) 

latex

Definitions	t.1, True, T, , A c B, x:A. B(x), P & Q, Knd, t  T, P  Q, x:A. B(x), {T}, SqStable(P),  k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v), x  {FDLNOr12445}
Lemmas	es-loc-rcv, ldst wf, true wf, squash wf, es-kind-rcv, es-sender wf, decidable assert, es-val wf, es-vartype wf, es-when wf, assert wf, sq stable from decidable, es-E wf, lsrc wf, es-loc wf, es-kind wf, Knd wf, IdLnk wf, Id wf, bool wf, event system wf, conditional-send1-p wf